A:Type, B:(AType), f:a:A fp B(a), eq:EqDecider(A), x:A, P:(a:{a:A| a  dom(f)} B(a)).
(z != f(x)  P(x,z))   

latex

Definitions	x:A. B(x), x(s), , t  T, z != f(x)  P(a;z), x(s1,s2), P  Q, x. t(x)
Lemmas	assert wf, fpf-dom wf, fpf-trivial-subtype-top, fpf-ap wf, deq wf, fpf wf